T:Type{i}, L:(T List), R:({x:T| (x  L)} es_realizer{i:l}),
P:({x:T| (x  L)} event_system{i:l}prop{i':l}).
l_all(L; T; x.R-realizes{i:l}(R(x); es.P(x,es)))
 l_all(L; T; x.l_all(L; T; y.(R-compat{i:l}(R(x); R(y))  (x = y  T))))
 R-realizes{i:l}
 R-realizes(Rall(L; x.R(x)); es.l_all(L; T; x.P(x,es))) 

latex

Definitions	x. t(x), t  T, P  Q, P  Q, x(s1,s2), x(s), R-realizes{i:l}(R; es.P(es)), l_all(L; T; x.P(x)), P  Q, prop{i:l}, x:A. B(x), P  Q
Lemmas	R-consistent-Rall, R-feasible-Rall, es realizer wf, R-Feasible wf, R-compat wf, event system wf, Rall wf, R-consistent wf, l member wf